\begin{tabbing}
($x$ unchanged{-}for $t$ @ $e$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=($\uparrow$$x$ changed before $e$)\+
\\[0ex]$\Rightarrow$ qle((es{-}time(${\it es}$; (last change to $x$ before $e$)) + $t$); es{-}time(${\it es}$; $e$))
\-
\end{tabbing}